package com.googlecode.kipler.satisfiability.completion.rule.individual;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.World;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.container.dl.operational.IndividualNameManager;
import com.googlecode.kipler.satisfiability.completion.rule.CompletionRule;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.ConceptDefinition;


/**
 * 
 * @author İnanç Seylan
 *
 */
public class NegatedConceptDefinitionRule extends CompletionRule {
	private ABox aBox;

	private boolean applied;

	public NegatedConceptDefinitionRule() {
		super();
	}

	public NegatedConceptDefinitionRule(WorldConstraintSystem wcs, World world) {
		super(wcs, world);
	}

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		aBox = getWorld().getABox();
		for (ConceptDefinition conDef : getWorld().getTBox().getGeneral()
				.getNegatedGCEs()) {
			applyNonEquality(conDef);
		}
	}

	public boolean isApplied() {
		return applied;
	}

	private void applyNonEquality(ConceptDefinition conDef)
			throws UnsatisfiableException {
		boolean negConceptExists = false;
		Concept negConcept = conDef.getLhs().copy().toggleNegated();
		for (Iterator<Individual> i = aBox.individualIterator(); i.hasNext();) {
			Individual indv = i.next();
			if (aBox.contains(new ConceptAssertion(negConcept, indv.getName()))) {
				negConceptExists = true;
				break;
			}
		}
		if (!negConceptExists) {
			String newIndv = IndividualNameManager.getInstance()
					.generateIndividualName();
			ConceptAssertion ca = new ConceptAssertion(negConcept, newIndv);
			getWcs().getData().getLogger().info(
					"WCS " + getWcs().getId()
							+ " Negated concept definition rule: Generating "
							+ newIndv + " adding " + ca);
			aBox.add(ca);
			applied = true;
		}
	}
}
